\begin{tabbing}
$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$, $B$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$;${\it da}$).
\\[0ex]ecl{-}trans{-}normal($A$)
\\[0ex]$\Rightarrow$ ecl{-}trans{-}normal($B$)
\\[0ex]$\Rightarrow$ (\=$\forall$$n$:$\mathbb{N}$, ${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List.\+
\\[0ex]ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$A$)($n$,${\it L'}$)
\\[0ex]$\Rightarrow$ ($\forall$$L$:event{-}info(${\it ds}$;${\it da}$) List. ${\it L'}$ $\leq$ $L$ $\Rightarrow$ ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$A$)($n$,$L$)))
\-\\[0ex]$\Rightarrow$ (\=$\forall$$n$:$\mathbb{N}$, ${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List.\+
\\[0ex]ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$B$)($n$,${\it L'}$)
\\[0ex]$\Rightarrow$ ($\forall$$L$:event{-}info(${\it ds}$;${\it da}$) List. ${\it L'}$ $\leq$ $L$ $\Rightarrow$ ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$B$)($n$,$L$)))
\-\\[0ex]$\Rightarrow$ (\=$\forall$$n$:$\mathbb{N}^{+}$, $L$:event{-}info(${\it ds}$;${\it da}$) List.\+
\\[0ex]ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$A$)($n$,$L$) $\Rightarrow$ ($n$ $\in$ ecl{-}trans{-}es($A$)))
\-\\[0ex]$\Rightarrow$ (\=$\forall$$n$:$\mathbb{N}^{+}$, $L$:event{-}info(${\it ds}$;${\it da}$) List.\+
\\[0ex]ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$B$)($n$,$L$) $\Rightarrow$ ($n$ $\in$ ecl{-}trans{-}es($B$)))
\-\\[0ex]$\Rightarrow$ (\=$\forall$\=$f$:(($\mathbb{B}$+Unit)$\rightarrow$($\mathbb{N}\rightarrow\mathbb{B}$)$\rightarrow$($\mathbb{N}\rightarrow\mathbb{B}$)$\rightarrow\mathbb{N}\rightarrow\mathbb{B}$), $g$:($\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}$),\+\+
\\[0ex]$L$:event{-}info(${\it ds}$;${\it da}$) List.
\-\\[0ex]$\exists$$x$:$\mathbb{B}$+Unit.
\\[0ex]ecl{-}trans{-}state(combine{-}ecl{-}tuples2($A$;$B$;$f$;$g$);$L$)
\\[0ex]$=$
\\[0ex]$\langle$ecl{-}trans{-}state($A$;$L$)$,\,$ecl{-}trans{-}state($B$;$L$)$,\,$$x$$\rangle$
\\[0ex]$\in$ ecl{-}trans{-}type(combine{-}ecl{-}tuples2($A$;$B$;$f$;$g$))
\\[0ex]\& (\=$x$ $=$ inl(true$_{2}$)\+
\\[0ex]$\Leftrightarrow$
\\[0ex](\=$\exists$${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List, $m$:$\mathbb{N}$.\+
\\[0ex]${\it L'}$ $\leq$ $L$
\\[0ex]\& ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$A$)($m$,${\it L'}$)
\\[0ex]\& (\=$\forall$$n$:$\mathbb{N}$, ${\it L''}$:event{-}info(${\it ds}$;${\it da}$) List.\+
\\[0ex]${\it L''}$ $\leq$ ${\it L'}$ $\Rightarrow$ ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$B$)($n$,${\it L''}$) $\Rightarrow$ ${\it L''}$ $=$ ${\it L'}$)
\-\\[0ex]\& ($\forall$$n$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$. $\neg$ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$B$)($n$,${\it L'}$))))
\-\-\\[0ex]\& (\=$x$ $=$ inl(false$_{2}$)\+
\\[0ex]$\Leftrightarrow$
\\[0ex](\=$\exists$${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List, $m$:$\mathbb{N}$.\+
\\[0ex]${\it L'}$ $\leq$ $L$
\\[0ex]\& ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$B$)($m$,${\it L'}$)
\\[0ex]\& (\=$\forall$$n$:$\mathbb{N}$, ${\it L''}$:event{-}info(${\it ds}$;${\it da}$) List.\+
\\[0ex]${\it L''}$ $\leq$ ${\it L'}$ $\Rightarrow$ ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$A$)($n$,${\it L''}$) $\Rightarrow$ ${\it L''}$ $=$ ${\it L'}$)
\-\\[0ex]\& ($\forall$$n$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$m$+1}}$. $\neg$ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$A$)($n$,${\it L'}$))))
\-\-\\[0ex]\& (\=$\neg$isl($x$)\+
\\[0ex]$\Leftrightarrow$
\\[0ex]($\forall$$m$:$\mathbb{N}$. $\neg$ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$A$)($m$,$L$) \& $\neg$ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$B$)($m$,$L$))))
\-\-
\end{tabbing}